state\_when($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$when{-}after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$).1